COMMENT ⊗   VALID 00003 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	
 00003 00003	
 00004 ENDMK
⊗;


STANFORD ARTIFICIAL INTELLIGENCE PROJECT              SEPTEMBER 1973
OPERATING NOTE 73







.BEGIN CENTER





PRELIMINARY USER'S MANUAL
FOR
AN
INTERACTIVE THEOREM PROVER

BY

JOHN ALLEN
.END










ABSTRACT:


.BEGIN DOUBLE SPACE
This document represents a short guide to using a development of the program
originally described in Allen and Luckham [MI5].  Many of the later sections,
on pattern matching and subroutining especially, are still in a rudimentary
stage of development. Experiments demonstrating various applications of the strategies
and the user oriented features are described in a forthcoming report,
"Applications of First Order Proof Procedures" by Allen, Luckham, and Morales.
.END